package ch.epfl.lara.matcheck.verify.provers.formdecider;

import java.io._

object FormDeciderWrapper extends FormulaDecider {
	/** Initializes the formula decider, returns whether the operation was successful */
	override def init: Boolean = {
		this.init(null, null)
	}

	/** Initializes the formula decider, controlling its output streams  */
        override def init(outStream: java.io.PrintStream, errStream: java.io.PrintStream): Boolean = {
		try {
			val (retVal, out, err) = executeCommand(Config.PROVER_EXEC)
			
			if(outStream != null) outStream.print(out)
			if(errStream != null) errStream.print(err)
				
			(retVal == 0 && out.contains("proof") && err.trim.length == 0)
		} catch {
			case e: Exception => e.printStackTrace; false
		}
	}

	/** Decides whether a formula is valid or not */
	override def decide(formula: String): ProverResults.ProverResult = {
      this.decide(formula, null, null)
	}
	
	
	/** Decides whether a formula is valid or not, controlling the output streams */
        override def decide(formula: String, outStream: java.io.PrintStream, errStream: java.io.PrintStream): ProverResults.ProverResult = {
		try {
			val temp: File = File.createTempFile("formDeciderFormula", "")
		
			val out: BufferedWriter = new BufferedWriter(new FileWriter(temp))
			out.write(formula)
			out.close
			
			val (retVal, output, errors) = executeCommand(Config.PROVER_EXEC + " " + temp.getAbsolutePath + " " +Config.PROVER_OPTIONS)
		
			if(outStream != null) outStream.print(output)
			if(errStream != null) errStream.print(errors)

			if(output.contains("VALID")) ProverResults.Valid
                        else if (errors.contains("timeout")) ProverResults.Timeout
                        else ProverResults.Invalid
		} catch {
			case e @ _ => 
                            e.printStackTrace; 
                            ProverResults.Invalid
		}		
	}

	/** Runs a command and returns the exit value, and the output and errors in two strings */
	def executeCommand(command: String): (Int, String, String) = {
                val rt: Runtime = Runtime.getRuntime();
                
		val proc:Process = rt.exec(command);
		
		val stderr: BufferedReader = new BufferedReader(
			new InputStreamReader(
				proc.getErrorStream()));

		val stdout: BufferedReader = new BufferedReader(
			new InputStreamReader(
				proc.getInputStream()));

		val exitValue: Int = proc.waitFor();

		var errors: String = "";
		var output: String = "";
		var buffer: String = "";

		buffer = stderr.readLine();
		while(buffer != null) {
			errors = errors + buffer + "\n"
			buffer = stderr.readLine();
		}
		stderr.close;

		buffer = stdout.readLine();
		while(buffer != null) {
			output = output + buffer + "\n"
			buffer = stdout.readLine();
		}
		stdout.close;

		(exitValue, output, errors)
          
	}
        
        
}
